T:Type, L1, L2, L:T List. interleaving(T;L1;L2;L)  Prop 

latex

Definitions	t  T, x:A. B(x), ||as||, ij, P  Q, False, A, AB, , disjoint_sublists(T;L1;L2;L), Prop, P & Q, interleaving(T;L1;L2;L)
Lemmas	nat wf, disjoint sublists wf, non neg length, length wf1